Nuprl Lemma : fadd_wf
4,23
postcript
pdf
n
,
m
,
k
:
,
f
:(
n
m
),
g
:(
n
(
k
+1)). fadd(
f
;
g
)
n
(
m
+
k
)
latex
Definitions
{
i
..
j
}
,
fadd(
f
;
g
)
,
A
B
,
A
,
False
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
t
T
,
i
j
<
k
,
P
&
Q
Lemmas
nat
wf
,
int
seg
wf
origin
n, m, k:
, f:(n
m), g:(n(k+1)). fadd(f;g) 
n(m+k) n, m, k:, f:(nm), g:(n(k+1)). fadd(f;g) n(m+k) 
}
B
A
Qx:A. B(x) T j < k